Inference at * 1 1 1 2 3 
Iof proof for Lemma comp nat ind tp:



1. P : {k}
2. i:. (j:. (j < i)  P(j))  P(i)
3. i : 
4. (i < (i + 1))  P(i)
  P(i) 

latex

 by (D (-1)) 

latex

 1: .....antecedent..... NILNIL

 1: 3. i : 
 1:   i < (i + 1)
 2: 

 2: 4. P(i)
 2:   P(i)
 .

Definitions

P  Q